$\forall$$M$:MsgA. Feasible($M$) $\Rightarrow$ AtomFree(Type;$M$.state)